A, B:Realizer.
R-Feasible(A)  R-Feasible(B)  A || B  (i:Id. R-state(A;i) || R-state(B;i)) 

latex

Definitions

ff, tt, True, T, x(s), P  Q, P  Q, P & Q, if b then t else f fi , x. t(x), Top, , {T}, SQType(T), R-ds(R;i), i  j , False, A, A  B, t  T, , R-state(R;i), P  Q, x:A. B(x), Unit, , A c B, P  Q, Y, A || B, ,

Lemmas

Rds wf, ifthenelse wf, fpf-empty wf, not functionality wrt iff, Id sq, assert-eq-id, R-loc wf, eq id wf, R-ds-Rds, deq wf, true wf, squash wf, fpf-compatible wf, fpf-empty-compatible-right, top wf, fpf wf, fpf-trivial-subtype-top, fpf-empty-compatible-left, Rnone-implies, Rnone? wf, fpf-compatible-join, Rplus-right wf, Rplus-left wf, R-ds wf, id-deq wf, fpf-compatible-join2, R-size-decreases, R-Feasible-Rplus, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, Rplus-implies, eqtt to assert, bool wf, bool sq, Rplus? wf, bool cases, ge wf, nat properties, es realizer wf, R-Feasible wf, R-compat wf, Id wf, le wf, nat plus wf, R-size wf, nat wf